interleaved_family_occurence(T;I;L;L2;f)
== (i:I. increasing(f(i);||L(i)||) & (j:||L(i)||. (L(i))[j] = L2[f(i,j)]))
== & (i1, i2:I. i1 = i2  (j1:||L(i1)||, j2:||L(i2)||. f(i1,j1) = f(i2,j2)))
== & (x:||L2||. i:I, j:||L(i)||. x = f(i,j)) 

latex

---

clarification:

interleaved_family_occurence(T;I;L;L2;f)
== (i:I. increasing(f(i);||L(i)||) & (j:{0..||L(i)||}. (L(i))[j] = L2[f(i,j)]  T))
== & (i1:I, i2:I.
== & (i1 = i2  I  (j1:{0..||L(i1)||}, j2:{0..||L(i2)||}. f(i1,j1) = f(i2,j2)  ))
== & (x:{0..||L2||}. i:I, j:{0..||L(i)||}. x = f(i,j)  ) 

latex

Definitions	P & Q, increasing(f;k), l[i], P  Q, A, x:A. B(x), x:A. B(x), {i..j}, ||as||
FDL editor aliases	interleaved_family_occurence